\chapter{Getting and Installing \HOL{}}
\label{install}

This chapter describes how to get the \HOL{} system and how to install
it.  It is generally assumed that some sort of Unix system is being
used, but the instructions that follow should apply {\it mutatis
  mutandis\/} to other platforms.  Unix is not a pre-requisite for
using the system. \HOL{} may be run on PCs running Windows operating
systems from Windows~NT onwards (i.e., Windows~2000, XP and Vista are
also supported), as well as Macintoshes running MacOS~X.

\section{Getting \HOL{}}

The \HOL{} system can be downloaded from \url{http://hol-theorem-prover.org}.
The naming scheme for \holn{} releases is $\langle${\it name}$\rangle$-$\langle${\it number}$\rangle$; the release described here is \holnversion.

\section{The {\tt hol-info} mailing list}

The \texttt{hol-info} mailing list serves as a forum for discussing
\HOL{} and disseminating news about it.  If you wish to be on this
list (which is recommended for all users of \HOL), visit
\url{http://lists.sourceforge.net/lists/listinfo/hol-info}.  This
web-page can also be used to unsubscribe from the mailing list.

\section{Installing \HOL{}}

It is assumed that the \HOL{} sources have been obtained and the
\texttt{tar} file unpacked into a directory \ml{hol}.\footnote{You may
  choose another name if you want; it is not important.} The contents
of this directory are likely to change over time, but it should
contain the following:

\begin{center}
\begin{tabular}{|l|l|l|} \hline
\multicolumn{3}{|c|}{ } \\
\multicolumn{3}{|c|}{\bf Principal Files on the HOL Distribution Directory} \\
\multicolumn{3}{|c|}{ } \\
{\it File name} & {\it Description} & {\it File type}  \\ \hline
{\tt README} & Description of directory {\tt hol} & Text\\
{\tt COPYRIGHT}& A copyright notice & Text\\
{\tt INSTALL} & Installation instructions & Text\\
{\tt tools} & Source code for building the system & Directory\\
{\tt bin} & Directory for HOL executables & Directory\\
{\tt sigobj} & Directory for \ML{} object files & Directory\\
{\tt src} & \ML{} sources of \HOL & Directory\\
{\tt help} & Help files for \HOL{} system & Directory\\
{\tt examples} & Example source files & Directory\\
\hline
\end{tabular}
\end{center}

The session in the box below shows a typical distribution directory.
The \HOL{} distribution has been placed on a PC running Linux in the
directory {\small\tt /home/mn200/hol/}.

All sessions in this documentation will be displayed in boxes with a
number in the top right hand corner.  This number indicates whether
the session is a new one (when the number will be {\small\sl 1}) or
the continuation of a session started in an earlier box.
Consecutively numbered boxes are assumed to be part of a single
continuous session.  The Unix prompt for the sessions is
\texttt{\small \dol}, so lines beginning with this prompt were typed
by the user.  After entering the \HOL{} system (see below), the user
is prompted with {\small\verb|-|} for an expression or command of the
\HOL{} meta-language \ML; lines beginning with this are thus \ML\
expressions or declarations.  Lines not beginning with \texttt{\small
  \$} or {\small\verb|-|} are system output.  Occasionally, system
output will be replaced with a line containing {\small\verb|...|} when
it is of minimal interest. The meta-language \ML{} is introduced in
Chapter~\ref{ML}.

\setcounter{sessioncount}{0}
\begin{session}
\begin{verbatim}
$ pwd
/home/mn200/hol
$ ls -F
CONTRIBUTORS    README          doc/            sigobj/         tools/
COPYRIGHT       bin/            examples/       src/            tools-poly/
INSTALL         developers/     help/           std.prelude
\end{verbatim}
\end{session}

Now you will need to rebuild \HOL{} from the sources.\footnote{It is
  possible that pre-built systems may soon be available from the
  web-page mentioned above.}

Before beginning you must have a current version of Poly/ML or Moscow~ML.\footnote{We recommend using Poly/ML on all operating systems, but it requires Cygwin or the Windows Linux sub-system on Windows.}
In the case of Moscow~ML, you must have at least version 2.01.
Poly/ML is available from \url{http://polyml.org}.
Moscow~ML is available on the web from \url{http://mosml.org}.

When working with Poly/ML, the installation must ensure that dynamic library loading (typically done by setting the \texttt{LD\_LIBRARY\_PATH} environment variable) picks up \texttt{libpolyml.so} and \texttt{libpolymain.so}.
If these files are in \texttt{/usr/lib}, nothing will need to be changed, but other locations may require further system configuration.
A sample \texttt{LD\_LIBRARY\_PATH} initialisation command (in a file such as \texttt{.bashrc}) might be
\begin{verbatim}
   declare -x LD_LIBRARY_PATH=/usr/local/lib:$HOME/lib
\end{verbatim}
Do not use the \texttt{--with-portable} option.

When you have your ML system installed, and are in the root directory of the distribution, the next step is to run \texttt{smart-configure}.
With Moscow~ML, this looks like:

\begin{session}
\begin{alltt}
\dol mosml < tools/smart-configure.sml
Moscow ML version 2.01 (January 2004)
Enter `quit();' to quit.
- [opening file "tools/smart-configure-mosml.sml"]

HOL smart configuration.

Determining configuration parameters: OS mosmldir holdir
OS:                 linux
mosmldir:           /home/mn200/mosml/bin
holdir:             /home/mn200/hol
dynlib_available:   true

Configuration will begin with above values.  If they are wrong
press Control-C.
\end{alltt}
\end{session}

If you are using Poly/ML, then write
\begin{verbatim}
   poly < tools/smart-configure.sml
\end{verbatim}
instead.

Assuming you don't interrupt the configuration process, this will
build the \texttt{Holmake} and \texttt{build} programs, and move them
into the \texttt{hol/bin} directory.  If something goes wrong at this
stage, consult Section~\ref{sec:editting-configure} below.

The next step is to run the \texttt{build} program.  This should
result in a great deal of output as all of the system code is compiled
and the theories built.  Eventually, a \HOL{} system\footnote{Four
  \HOL{} executables are produced: \textsf{hol}, \textsf{hol.noquote},
  \textsf{hol.bare} and \textsf{hol.bare.noquote}.  The first of these
  will be used for most examples in the \TUTORIAL{}.} is produced in
the \texttt{bin/} directory.

\begin{session}
\begin{alltt}
\dol bin/build
  ...
  ...
Uploading files to /home/mn200/hol/sigobj

Hol built successfully.
\dol
\end{alltt}
\end{session}

At this point, the system is build in your HOL directory, and cannot easily be moved to other locations.
In other words, you should unpack HOL in the location/directory where you wish to access it for all your future work.



\subsection{Overriding \texttt{smart-configure}}
\label{sec:editting-configure}

If \texttt{smart-configure} is unable to guess correct values for the various parameters (\texttt{holdir}, \texttt{OS} \etc) then you can create a file called to provide correct values.
With Poly/ML, this should be \texttt{poly-includes.ML} in the \texttt{tools-poly} directory.
With Moscow~ML, this should be \texttt{config-override} in the root directory of the HOL distribution.
In this file, specify the correct value for the appropriate parameter by providing an ML binding for it.
All variables except \texttt{dynlib\_available} must be given a string as a possible value, while \texttt{dynlib\_available} must be either \texttt{true} or \texttt{false}.
So, one might write

\begin{session}
\begin{verbatim}
val OS = "unix";
val holdir = "/local/scratch/myholdir";
val dynlib_available = false;
\end{verbatim}
\end{session}

The \texttt{config-override} file need only provide values for those
variables that need overriding.

With this file in place, the \texttt{smart-configure} program will use
the values specified there rather than those it attempts to calculate
itself.  The value given for the \texttt{OS} variable must be one of
\texttt{"unix"}, \texttt{"linux"}, \texttt{"solaris"},
\texttt{"macosx"} or \texttt{"winNT"}.\footnote{%
The string \texttt{"winNT"} is used for Microsoft Windows operating systems that are at least as recent as Windows~NT.
This includes Windows~2000, XP, Vista, Windows~10 \textit{etc}.
Do not use \texttt{"winNT"} when using Poly/ML \textit{via} Cygwin or the Linux sub-system.}

In extreme circumstances it is possible to edit the file
\texttt{tools/configure.sml} yourself to set configuration variables
directly.  (If you are using Poly/ML, you must edit
\texttt{tools-poly/configure.sml} instead.) At the top of this file
various incomplete SML declarations are present, but commented out.
You will need to uncomment this section (remove the \texttt{(*} and
\texttt{*)} markers), and provide sensible values.  All strings must
be enclosed in double quotes.

The \texttt{holdir} value must be the name of the top-level directory
listed in the first session above.  The \texttt{OS} value should be
one of the strings specified in the accompanying comment.

When working with Poly/ML, the \texttt{poly} string must be the path to the \texttt{poly} executable that begins an interactive \ML{} session.
The \texttt{polymllibdir} must be a path to a directory that contains the file \texttt{libpolymain.a}.
When working with Moscow~ML, the \texttt{mosmldir} value must be the
name of the directory containing the Moscow~ML binaries
(\texttt{mosmlc}, \texttt{mosml}, \texttt{mosmllex} etc).

Subsequent values (\texttt{CC} and \texttt{GNUMAKE}) are needed for
``optional'' components of the system.  The first gives a string
suitable for invoking the system's C compiler, and the second
specifies a \textsf{make} program.

After editing, \texttt{tools/configure.sml} the lines above will look
something like:

\begin{session}
\begin{alltt}
\dol more configure.sml
  ...
val mosmldir = "/home/mn200/mosml";
val holdir   = "/home/mn200/hol";
val OS       = "linux"       (* Operating system; choices are:
                                "linux", "solaris", "unix", "winNT" *)

val CC       = "gcc";     (* C compiler (for building quote filter)        *)
val GNUMAKE  = "gnumake"; (* for robdd library                             *)
  ...
\dol
\end{alltt}
\end{session}

\noindent Now, at either this level (in the \texttt{tools} or
\texttt{tools-poly} directory) or at the level above, the script
\texttt{configure.sml} must be piped into the \ML{} interpreter (\ie,
\texttt{mosml} or \texttt{poly}).  For example,

\begin{session}
\begin{alltt}
\dol mosml < tools/configure.sml
Moscow ML version 2.01 (January 2004)
Enter `quit();' to quit.
- > val mosmldir = "/home/mn200/mosml" : string
  val holdir = "/home/mn200/hol" : string
  val OS = "linux" : string
- > val CC = "gcc" : string
  ...
Beginning configuration.
- Making bin/Holmake.
  ...
Making bin/build.
- Making hol98-mode.el (for Emacs)
- Setting up the standard prelude.
- Setting up src/0/Globals.sml.
- Generating bin/hol.
- Generating bin/hol.noquote.
- Attempting to compile quote filter ... successful.
- Setting up the muddy library Makefile.
- Setting up the help Makefile.
-
Finished configuration!
-
\dol
\end{alltt}
\end{session}



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "tutorial"
%%% End:
